The Runtime Complexity (full) of the given CpxTRS could be proven to be BOUNDS(n^2, INF).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

Term_sub(Case(m, xi, n), s) → Frozen(m, Sum_sub(xi, s), n, s)
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s)
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s)
Frozen(m, Sum_term_var(xi), n, s) → Case(Term_sub(m, s), xi, Term_sub(n, s))
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s))
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s))
Term_sub(Term_var(x), Id) → Term_var(x)
Term_sub(Term_var(x), Cons_usual(y, m, s)) → m
Term_sub(Term_var(x), Cons_usual(y, m, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_var(x), Cons_sum(xi, k, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_sub(m, s), t) → Term_sub(m, Concat(s, t))
Sum_sub(xi, Id) → Sum_term_var(xi)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_constant(k)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_sub(xi, s)
Sum_sub(xi, Cons_usual(y, m, s)) → Sum_sub(xi, s)
Concat(Concat(s, t), u) → Concat(s, Concat(t, u))
Concat(Cons_usual(x, m, s), t) → Cons_usual(x, Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(xi, k, s), t) → Cons_sum(xi, k, Concat(s, t))
Concat(Id, s) → s

Rewrite Strategy: FULL

(1) DecreasingLoopProof (EQUIVALENT transformation)

The following loop(s) give(s) rise to the lower bound Ω(n¹):
The rewrite sequence
Term_sub(Case(m, xi, n), Id) →⁺ Case(Term_sub(m, Id), xi, Term_sub(n, Id))
gives rise to a decreasing loop by considering the right hand sides subterm at position [0].
The pumping substitution is [m / Case(m, xi, n)].
The result substitution is [ ].

(2) BOUNDS(n^1, INF)

(3) RenamingProof (EQUIVALENT transformation)

Renamed function symbols to avoid clashes with predefined symbol.

(4) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

Term_sub(Case(m, xi, n), s) → Frozen(m, Sum_sub(xi, s), n, s)
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s)
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s)
Frozen(m, Sum_term_var(xi), n, s) → Case(Term_sub(m, s), xi, Term_sub(n, s))
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s))
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s))
Term_sub(Term_var(x), Id) → Term_var(x)
Term_sub(Term_var(x), Cons_usual(y, m, s)) → m
Term_sub(Term_var(x), Cons_usual(y, m, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_var(x), Cons_sum(xi, k, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_sub(m, s), t) → Term_sub(m, Concat(s, t))
Sum_sub(xi, Id) → Sum_term_var(xi)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_constant(k)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_sub(xi, s)
Sum_sub(xi, Cons_usual(y, m, s)) → Sum_sub(xi, s)
Concat(Concat(s, t), u) → Concat(s, Concat(t, u))
Concat(Cons_usual(x, m, s), t) → Cons_usual(x, Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(xi, k, s), t) → Cons_sum(xi, k, Concat(s, t))
Concat(Id, s) → s

S is empty.
Rewrite Strategy: FULL

(5) SlicingProof (LOWER BOUND(ID) transformation)

Sliced the following arguments:
Case/1
Sum_sub/0
Sum_term_var/0
Term_var/0
Cons_usual/0
Cons_sum/0

(6) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

Term_sub(Case(m, n), s) → Frozen(m, Sum_sub(s), n, s)
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s)
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s)
Frozen(m, Sum_term_var, n, s) → Case(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s))
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s))
Term_sub(Term_var, Id) → Term_var
Term_sub(Term_var, Cons_usual(m, s)) → m
Term_sub(Term_var, Cons_usual(m, s)) → Term_sub(Term_var, s)
Term_sub(Term_var, Cons_sum(k, s)) → Term_sub(Term_var, s)
Term_sub(Term_sub(m, s), t) → Term_sub(m, Concat(s, t))
Sum_sub(Id) → Sum_term_var
Sum_sub(Cons_sum(k, s)) → Sum_constant(k)
Sum_sub(Cons_sum(k, s)) → Sum_sub(s)
Sum_sub(Cons_usual(m, s)) → Sum_sub(s)
Concat(Concat(s, t), u) → Concat(s, Concat(t, u))
Concat(Cons_usual(m, s), t) → Cons_usual(Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(k, s), t) → Cons_sum(k, Concat(s, t))
Concat(Id, s) → s

S is empty.
Rewrite Strategy: FULL

(7) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(8) Obligation:

TRS:
Rules:
Term_sub(Case(m, n), s) → Frozen(m, Sum_sub(s), n, s)
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s)
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s)
Frozen(m, Sum_term_var, n, s) → Case(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s))
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s))
Term_sub(Term_var, Id) → Term_var
Term_sub(Term_var, Cons_usual(m, s)) → m
Term_sub(Term_var, Cons_usual(m, s)) → Term_sub(Term_var, s)
Term_sub(Term_var, Cons_sum(k, s)) → Term_sub(Term_var, s)
Term_sub(Term_sub(m, s), t) → Term_sub(m, Concat(s, t))
Sum_sub(Id) → Sum_term_var
Sum_sub(Cons_sum(k, s)) → Sum_constant(k)
Sum_sub(Cons_sum(k, s)) → Sum_sub(s)
Sum_sub(Cons_usual(m, s)) → Sum_sub(s)
Concat(Concat(s, t), u) → Concat(s, Concat(t, u))
Concat(Cons_usual(m, s), t) → Cons_usual(Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(k, s), t) → Cons_sum(k, Concat(s, t))
Concat(Id, s) → s

Types:
Term_sub :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Case :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Frozen :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Sum_constant:Sum_term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Sum_sub :: Id:Cons_usual:Cons_sum → Sum_constant:Sum_term_var
Sum_constant :: Left:Right → Sum_constant:Sum_term_var
Left :: Left:Right
Right :: Left:Right
Sum_term_var :: Sum_constant:Sum_term_var
Term_app :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_pair :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_inl :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_inr :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_var :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Id :: Id:Cons_usual:Cons_sum
Cons_usual :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
Cons_sum :: Left:Right → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
Concat :: Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
hole_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var1_0 :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
hole_Id:Cons_usual:Cons_sum2_0 :: Id:Cons_usual:Cons_sum
hole_Sum_constant:Sum_term_var3_0 :: Sum_constant:Sum_term_var
hole_Left:Right4_0 :: Left:Right
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0 :: Nat → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
gen_Id:Cons_usual:Cons_sum6_0 :: Nat → Id:Cons_usual:Cons_sum

(9) OrderProof (LOWER BOUND(ID) transformation)

Heuristically decided to analyse the following defined symbols:
Term_sub, Sum_sub, Concat

They will be analysed ascendingly in the following order:
Sum_sub < Term_sub
Term_sub = Concat

(10) Obligation:

TRS:
Rules:
Term_sub(Case(m, n), s) → Frozen(m, Sum_sub(s), n, s)
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s)
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s)
Frozen(m, Sum_term_var, n, s) → Case(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s))
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s))
Term_sub(Term_var, Id) → Term_var
Term_sub(Term_var, Cons_usual(m, s)) → m
Term_sub(Term_var, Cons_usual(m, s)) → Term_sub(Term_var, s)
Term_sub(Term_var, Cons_sum(k, s)) → Term_sub(Term_var, s)
Term_sub(Term_sub(m, s), t) → Term_sub(m, Concat(s, t))
Sum_sub(Id) → Sum_term_var
Sum_sub(Cons_sum(k, s)) → Sum_constant(k)
Sum_sub(Cons_sum(k, s)) → Sum_sub(s)
Sum_sub(Cons_usual(m, s)) → Sum_sub(s)
Concat(Concat(s, t), u) → Concat(s, Concat(t, u))
Concat(Cons_usual(m, s), t) → Cons_usual(Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(k, s), t) → Cons_sum(k, Concat(s, t))
Concat(Id, s) → s

Types:
Term_sub :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Case :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Frozen :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Sum_constant:Sum_term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Sum_sub :: Id:Cons_usual:Cons_sum → Sum_constant:Sum_term_var
Sum_constant :: Left:Right → Sum_constant:Sum_term_var
Left :: Left:Right
Right :: Left:Right
Sum_term_var :: Sum_constant:Sum_term_var
Term_app :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_pair :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_inl :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_inr :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_var :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Id :: Id:Cons_usual:Cons_sum
Cons_usual :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
Cons_sum :: Left:Right → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
Concat :: Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
hole_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var1_0 :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
hole_Id:Cons_usual:Cons_sum2_0 :: Id:Cons_usual:Cons_sum
hole_Sum_constant:Sum_term_var3_0 :: Sum_constant:Sum_term_var
hole_Left:Right4_0 :: Left:Right
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0 :: Nat → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
gen_Id:Cons_usual:Cons_sum6_0 :: Nat → Id:Cons_usual:Cons_sum

Generator Equations:
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(0) ⇔ Term_var
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(+(x, 1)) ⇔ Case(Term_var, gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(x))
gen_Id:Cons_usual:Cons_sum6_0(0) ⇔ Id
gen_Id:Cons_usual:Cons_sum6_0(+(x, 1)) ⇔ Cons_usual(Term_var, gen_Id:Cons_usual:Cons_sum6_0(x))

The following defined symbols remain to be analysed:
Sum_sub, Term_sub, Concat

They will be analysed ascendingly in the following order:
Sum_sub < Term_sub
Term_sub = Concat

(11) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
Sum_sub(gen_Id:Cons_usual:Cons_sum6_0(n8_0)) → Sum_term_var, rt ∈ Ω(1 + n8₀)

Induction Base:
Sum_sub(gen_Id:Cons_usual:Cons_sum6_0(0)) →_R^Ω(1)
Sum_term_var

Induction Step:
Sum_sub(gen_Id:Cons_usual:Cons_sum6_0(+(n8_0, 1))) →_R^Ω(1)
Sum_sub(gen_Id:Cons_usual:Cons_sum6_0(n8_0)) →_IH
Sum_term_var

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(12) Complex Obligation (BEST)

(13) Obligation:

TRS:
Rules:
Term_sub(Case(m, n), s) → Frozen(m, Sum_sub(s), n, s)
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s)
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s)
Frozen(m, Sum_term_var, n, s) → Case(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s))
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s))
Term_sub(Term_var, Id) → Term_var
Term_sub(Term_var, Cons_usual(m, s)) → m
Term_sub(Term_var, Cons_usual(m, s)) → Term_sub(Term_var, s)
Term_sub(Term_var, Cons_sum(k, s)) → Term_sub(Term_var, s)
Term_sub(Term_sub(m, s), t) → Term_sub(m, Concat(s, t))
Sum_sub(Id) → Sum_term_var
Sum_sub(Cons_sum(k, s)) → Sum_constant(k)
Sum_sub(Cons_sum(k, s)) → Sum_sub(s)
Sum_sub(Cons_usual(m, s)) → Sum_sub(s)
Concat(Concat(s, t), u) → Concat(s, Concat(t, u))
Concat(Cons_usual(m, s), t) → Cons_usual(Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(k, s), t) → Cons_sum(k, Concat(s, t))
Concat(Id, s) → s

Types:
Term_sub :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Case :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Frozen :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Sum_constant:Sum_term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Sum_sub :: Id:Cons_usual:Cons_sum → Sum_constant:Sum_term_var
Sum_constant :: Left:Right → Sum_constant:Sum_term_var
Left :: Left:Right
Right :: Left:Right
Sum_term_var :: Sum_constant:Sum_term_var
Term_app :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_pair :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_inl :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_inr :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_var :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Id :: Id:Cons_usual:Cons_sum
Cons_usual :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
Cons_sum :: Left:Right → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
Concat :: Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
hole_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var1_0 :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
hole_Id:Cons_usual:Cons_sum2_0 :: Id:Cons_usual:Cons_sum
hole_Sum_constant:Sum_term_var3_0 :: Sum_constant:Sum_term_var
hole_Left:Right4_0 :: Left:Right
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0 :: Nat → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
gen_Id:Cons_usual:Cons_sum6_0 :: Nat → Id:Cons_usual:Cons_sum

Lemmas:
Sum_sub(gen_Id:Cons_usual:Cons_sum6_0(n8_0)) → Sum_term_var, rt ∈ Ω(1 + n8₀)

Generator Equations:
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(0) ⇔ Term_var
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(+(x, 1)) ⇔ Case(Term_var, gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(x))
gen_Id:Cons_usual:Cons_sum6_0(0) ⇔ Id
gen_Id:Cons_usual:Cons_sum6_0(+(x, 1)) ⇔ Cons_usual(Term_var, gen_Id:Cons_usual:Cons_sum6_0(x))

The following defined symbols remain to be analysed:
Concat, Term_sub

They will be analysed ascendingly in the following order:
Term_sub = Concat

(14) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
Concat(gen_Id:Cons_usual:Cons_sum6_0(n370_0), gen_Id:Cons_usual:Cons_sum6_0(0)) → gen_Id:Cons_usual:Cons_sum6_0(n370_0), rt ∈ Ω(1 + n370₀)

Induction Base:
Concat(gen_Id:Cons_usual:Cons_sum6_0(0), gen_Id:Cons_usual:Cons_sum6_0(0)) →_R^Ω(1)
gen_Id:Cons_usual:Cons_sum6_0(0)

Induction Step:
Concat(gen_Id:Cons_usual:Cons_sum6_0(+(n370_0, 1)), gen_Id:Cons_usual:Cons_sum6_0(0)) →_R^Ω(1)
Cons_usual(Term_sub(Term_var, gen_Id:Cons_usual:Cons_sum6_0(0)), Concat(gen_Id:Cons_usual:Cons_sum6_0(n370_0), gen_Id:Cons_usual:Cons_sum6_0(0))) →_R^Ω(1)
Cons_usual(Term_var, Concat(gen_Id:Cons_usual:Cons_sum6_0(n370_0), gen_Id:Cons_usual:Cons_sum6_0(0))) →_IH
Cons_usual(Term_var, gen_Id:Cons_usual:Cons_sum6_0(c371_0))

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(15) Complex Obligation (BEST)

(16) Obligation:

TRS:
Rules:
Term_sub(Case(m, n), s) → Frozen(m, Sum_sub(s), n, s)
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s)
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s)
Frozen(m, Sum_term_var, n, s) → Case(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s))
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s))
Term_sub(Term_var, Id) → Term_var
Term_sub(Term_var, Cons_usual(m, s)) → m
Term_sub(Term_var, Cons_usual(m, s)) → Term_sub(Term_var, s)
Term_sub(Term_var, Cons_sum(k, s)) → Term_sub(Term_var, s)
Term_sub(Term_sub(m, s), t) → Term_sub(m, Concat(s, t))
Sum_sub(Id) → Sum_term_var
Sum_sub(Cons_sum(k, s)) → Sum_constant(k)
Sum_sub(Cons_sum(k, s)) → Sum_sub(s)
Sum_sub(Cons_usual(m, s)) → Sum_sub(s)
Concat(Concat(s, t), u) → Concat(s, Concat(t, u))
Concat(Cons_usual(m, s), t) → Cons_usual(Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(k, s), t) → Cons_sum(k, Concat(s, t))
Concat(Id, s) → s

Types:
Term_sub :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Case :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Frozen :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Sum_constant:Sum_term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Sum_sub :: Id:Cons_usual:Cons_sum → Sum_constant:Sum_term_var
Sum_constant :: Left:Right → Sum_constant:Sum_term_var
Left :: Left:Right
Right :: Left:Right
Sum_term_var :: Sum_constant:Sum_term_var
Term_app :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_pair :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_inl :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_inr :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_var :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Id :: Id:Cons_usual:Cons_sum
Cons_usual :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
Cons_sum :: Left:Right → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
Concat :: Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
hole_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var1_0 :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
hole_Id:Cons_usual:Cons_sum2_0 :: Id:Cons_usual:Cons_sum
hole_Sum_constant:Sum_term_var3_0 :: Sum_constant:Sum_term_var
hole_Left:Right4_0 :: Left:Right
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0 :: Nat → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
gen_Id:Cons_usual:Cons_sum6_0 :: Nat → Id:Cons_usual:Cons_sum

Lemmas:
Sum_sub(gen_Id:Cons_usual:Cons_sum6_0(n8_0)) → Sum_term_var, rt ∈ Ω(1 + n8₀)
Concat(gen_Id:Cons_usual:Cons_sum6_0(n370_0), gen_Id:Cons_usual:Cons_sum6_0(0)) → gen_Id:Cons_usual:Cons_sum6_0(n370_0), rt ∈ Ω(1 + n370₀)

Generator Equations:
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(0) ⇔ Term_var
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(+(x, 1)) ⇔ Case(Term_var, gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(x))
gen_Id:Cons_usual:Cons_sum6_0(0) ⇔ Id
gen_Id:Cons_usual:Cons_sum6_0(+(x, 1)) ⇔ Cons_usual(Term_var, gen_Id:Cons_usual:Cons_sum6_0(x))

The following defined symbols remain to be analysed:
Term_sub

They will be analysed ascendingly in the following order:
Term_sub = Concat

(17) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
Term_sub(gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(0), gen_Id:Cons_usual:Cons_sum6_0(n183948_0)) → gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(0), rt ∈ Ω(1 + n183948₀)

Induction Base:
Term_sub(gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(0), gen_Id:Cons_usual:Cons_sum6_0(0)) →_R^Ω(1)
Term_var

Induction Step:
Term_sub(gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(0), gen_Id:Cons_usual:Cons_sum6_0(+(n183948_0, 1))) →_R^Ω(1)
Term_sub(Term_var, gen_Id:Cons_usual:Cons_sum6_0(n183948_0)) →_IH
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(0)

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(18) Complex Obligation (BEST)

(19) Obligation:

TRS:
Rules:
Term_sub(Case(m, n), s) → Frozen(m, Sum_sub(s), n, s)
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s)
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s)
Frozen(m, Sum_term_var, n, s) → Case(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s))
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s))
Term_sub(Term_var, Id) → Term_var
Term_sub(Term_var, Cons_usual(m, s)) → m
Term_sub(Term_var, Cons_usual(m, s)) → Term_sub(Term_var, s)
Term_sub(Term_var, Cons_sum(k, s)) → Term_sub(Term_var, s)
Term_sub(Term_sub(m, s), t) → Term_sub(m, Concat(s, t))
Sum_sub(Id) → Sum_term_var
Sum_sub(Cons_sum(k, s)) → Sum_constant(k)
Sum_sub(Cons_sum(k, s)) → Sum_sub(s)
Sum_sub(Cons_usual(m, s)) → Sum_sub(s)
Concat(Concat(s, t), u) → Concat(s, Concat(t, u))
Concat(Cons_usual(m, s), t) → Cons_usual(Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(k, s), t) → Cons_sum(k, Concat(s, t))
Concat(Id, s) → s

Types:
Term_sub :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Case :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Frozen :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Sum_constant:Sum_term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Sum_sub :: Id:Cons_usual:Cons_sum → Sum_constant:Sum_term_var
Sum_constant :: Left:Right → Sum_constant:Sum_term_var
Left :: Left:Right
Right :: Left:Right
Sum_term_var :: Sum_constant:Sum_term_var
Term_app :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_pair :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_inl :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_inr :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_var :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Id :: Id:Cons_usual:Cons_sum
Cons_usual :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
Cons_sum :: Left:Right → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
Concat :: Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
hole_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var1_0 :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
hole_Id:Cons_usual:Cons_sum2_0 :: Id:Cons_usual:Cons_sum
hole_Sum_constant:Sum_term_var3_0 :: Sum_constant:Sum_term_var
hole_Left:Right4_0 :: Left:Right
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0 :: Nat → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
gen_Id:Cons_usual:Cons_sum6_0 :: Nat → Id:Cons_usual:Cons_sum

Lemmas:
Sum_sub(gen_Id:Cons_usual:Cons_sum6_0(n8_0)) → Sum_term_var, rt ∈ Ω(1 + n8₀)
Concat(gen_Id:Cons_usual:Cons_sum6_0(n370_0), gen_Id:Cons_usual:Cons_sum6_0(0)) → gen_Id:Cons_usual:Cons_sum6_0(n370_0), rt ∈ Ω(1 + n370₀)
Term_sub(gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(0), gen_Id:Cons_usual:Cons_sum6_0(n183948_0)) → gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(0), rt ∈ Ω(1 + n183948₀)

Generator Equations:
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(0) ⇔ Term_var
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(+(x, 1)) ⇔ Case(Term_var, gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(x))
gen_Id:Cons_usual:Cons_sum6_0(0) ⇔ Id
gen_Id:Cons_usual:Cons_sum6_0(+(x, 1)) ⇔ Cons_usual(Term_var, gen_Id:Cons_usual:Cons_sum6_0(x))

The following defined symbols remain to be analysed:
Concat

They will be analysed ascendingly in the following order:
Term_sub = Concat

(20) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
Concat(gen_Id:Cons_usual:Cons_sum6_0(n390070_0), gen_Id:Cons_usual:Cons_sum6_0(b)) → gen_Id:Cons_usual:Cons_sum6_0(+(n390070_0, b)), rt ∈ Ω(1 + b·n390070₀ + n390070₀)

Induction Base:
Concat(gen_Id:Cons_usual:Cons_sum6_0(0), gen_Id:Cons_usual:Cons_sum6_0(b)) →_R^Ω(1)
gen_Id:Cons_usual:Cons_sum6_0(b)

Induction Step:
Concat(gen_Id:Cons_usual:Cons_sum6_0(+(n390070_0, 1)), gen_Id:Cons_usual:Cons_sum6_0(b)) →_R^Ω(1)
Cons_usual(Term_sub(Term_var, gen_Id:Cons_usual:Cons_sum6_0(b)), Concat(gen_Id:Cons_usual:Cons_sum6_0(n390070_0), gen_Id:Cons_usual:Cons_sum6_0(b))) →_L^{Ω(1 + b)}
Cons_usual(gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(0), Concat(gen_Id:Cons_usual:Cons_sum6_0(n390070_0), gen_Id:Cons_usual:Cons_sum6_0(b))) →_IH
Cons_usual(gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(0), gen_Id:Cons_usual:Cons_sum6_0(+(b, c390071_0)))

We have rt ∈ Ω(n²) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n²).

(21) Complex Obligation (BEST)

(22) Obligation:

TRS:
Rules:
Term_sub(Case(m, n), s) → Frozen(m, Sum_sub(s), n, s)
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s)
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s)
Frozen(m, Sum_term_var, n, s) → Case(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s))
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s))
Term_sub(Term_var, Id) → Term_var
Term_sub(Term_var, Cons_usual(m, s)) → m
Term_sub(Term_var, Cons_usual(m, s)) → Term_sub(Term_var, s)
Term_sub(Term_var, Cons_sum(k, s)) → Term_sub(Term_var, s)
Term_sub(Term_sub(m, s), t) → Term_sub(m, Concat(s, t))
Sum_sub(Id) → Sum_term_var
Sum_sub(Cons_sum(k, s)) → Sum_constant(k)
Sum_sub(Cons_sum(k, s)) → Sum_sub(s)
Sum_sub(Cons_usual(m, s)) → Sum_sub(s)
Concat(Concat(s, t), u) → Concat(s, Concat(t, u))
Concat(Cons_usual(m, s), t) → Cons_usual(Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(k, s), t) → Cons_sum(k, Concat(s, t))
Concat(Id, s) → s

Types:
Term_sub :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Case :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Frozen :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Sum_constant:Sum_term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Sum_sub :: Id:Cons_usual:Cons_sum → Sum_constant:Sum_term_var
Sum_constant :: Left:Right → Sum_constant:Sum_term_var
Left :: Left:Right
Right :: Left:Right
Sum_term_var :: Sum_constant:Sum_term_var
Term_app :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_pair :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_inl :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_inr :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_var :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Id :: Id:Cons_usual:Cons_sum
Cons_usual :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
Cons_sum :: Left:Right → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
Concat :: Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
hole_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var1_0 :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
hole_Id:Cons_usual:Cons_sum2_0 :: Id:Cons_usual:Cons_sum
hole_Sum_constant:Sum_term_var3_0 :: Sum_constant:Sum_term_var
hole_Left:Right4_0 :: Left:Right
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0 :: Nat → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
gen_Id:Cons_usual:Cons_sum6_0 :: Nat → Id:Cons_usual:Cons_sum

Lemmas:
Sum_sub(gen_Id:Cons_usual:Cons_sum6_0(n8_0)) → Sum_term_var, rt ∈ Ω(1 + n8₀)
Concat(gen_Id:Cons_usual:Cons_sum6_0(n390070_0), gen_Id:Cons_usual:Cons_sum6_0(b)) → gen_Id:Cons_usual:Cons_sum6_0(+(n390070_0, b)), rt ∈ Ω(1 + b·n390070₀ + n390070₀)
Term_sub(gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(0), gen_Id:Cons_usual:Cons_sum6_0(n183948_0)) → gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(0), rt ∈ Ω(1 + n183948₀)

Generator Equations:
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(0) ⇔ Term_var
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(+(x, 1)) ⇔ Case(Term_var, gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(x))
gen_Id:Cons_usual:Cons_sum6_0(0) ⇔ Id
gen_Id:Cons_usual:Cons_sum6_0(+(x, 1)) ⇔ Cons_usual(Term_var, gen_Id:Cons_usual:Cons_sum6_0(x))

No more defined symbols left to analyse.

(23) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n²) was proven with the following lemma:
Concat(gen_Id:Cons_usual:Cons_sum6_0(n390070_0), gen_Id:Cons_usual:Cons_sum6_0(b)) → gen_Id:Cons_usual:Cons_sum6_0(+(n390070_0, b)), rt ∈ Ω(1 + b·n390070₀ + n390070₀)

(24) BOUNDS(n^2, INF)

(25) Obligation:

TRS:
Rules:
Term_sub(Case(m, n), s) → Frozen(m, Sum_sub(s), n, s)
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s)
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s)
Frozen(m, Sum_term_var, n, s) → Case(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s))
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s))
Term_sub(Term_var, Id) → Term_var
Term_sub(Term_var, Cons_usual(m, s)) → m
Term_sub(Term_var, Cons_usual(m, s)) → Term_sub(Term_var, s)
Term_sub(Term_var, Cons_sum(k, s)) → Term_sub(Term_var, s)
Term_sub(Term_sub(m, s), t) → Term_sub(m, Concat(s, t))
Sum_sub(Id) → Sum_term_var
Sum_sub(Cons_sum(k, s)) → Sum_constant(k)
Sum_sub(Cons_sum(k, s)) → Sum_sub(s)
Sum_sub(Cons_usual(m, s)) → Sum_sub(s)
Concat(Concat(s, t), u) → Concat(s, Concat(t, u))
Concat(Cons_usual(m, s), t) → Cons_usual(Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(k, s), t) → Cons_sum(k, Concat(s, t))
Concat(Id, s) → s

Types:
Term_sub :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Case :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Frozen :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Sum_constant:Sum_term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Sum_sub :: Id:Cons_usual:Cons_sum → Sum_constant:Sum_term_var
Sum_constant :: Left:Right → Sum_constant:Sum_term_var
Left :: Left:Right
Right :: Left:Right
Sum_term_var :: Sum_constant:Sum_term_var
Term_app :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_pair :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_inl :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_inr :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_var :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Id :: Id:Cons_usual:Cons_sum
Cons_usual :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
Cons_sum :: Left:Right → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
Concat :: Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
hole_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var1_0 :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
hole_Id:Cons_usual:Cons_sum2_0 :: Id:Cons_usual:Cons_sum
hole_Sum_constant:Sum_term_var3_0 :: Sum_constant:Sum_term_var
hole_Left:Right4_0 :: Left:Right
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0 :: Nat → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
gen_Id:Cons_usual:Cons_sum6_0 :: Nat → Id:Cons_usual:Cons_sum

Lemmas:
Sum_sub(gen_Id:Cons_usual:Cons_sum6_0(n8_0)) → Sum_term_var, rt ∈ Ω(1 + n8₀)
Concat(gen_Id:Cons_usual:Cons_sum6_0(n390070_0), gen_Id:Cons_usual:Cons_sum6_0(b)) → gen_Id:Cons_usual:Cons_sum6_0(+(n390070_0, b)), rt ∈ Ω(1 + b·n390070₀ + n390070₀)
Term_sub(gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(0), gen_Id:Cons_usual:Cons_sum6_0(n183948_0)) → gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(0), rt ∈ Ω(1 + n183948₀)

Generator Equations:
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(0) ⇔ Term_var
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(+(x, 1)) ⇔ Case(Term_var, gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(x))
gen_Id:Cons_usual:Cons_sum6_0(0) ⇔ Id
gen_Id:Cons_usual:Cons_sum6_0(+(x, 1)) ⇔ Cons_usual(Term_var, gen_Id:Cons_usual:Cons_sum6_0(x))

No more defined symbols left to analyse.

(26) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n²) was proven with the following lemma:
Concat(gen_Id:Cons_usual:Cons_sum6_0(n390070_0), gen_Id:Cons_usual:Cons_sum6_0(b)) → gen_Id:Cons_usual:Cons_sum6_0(+(n390070_0, b)), rt ∈ Ω(1 + b·n390070₀ + n390070₀)

(27) BOUNDS(n^2, INF)

(28) Obligation:

TRS:
Rules:
Term_sub(Case(m, n), s) → Frozen(m, Sum_sub(s), n, s)
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s)
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s)
Frozen(m, Sum_term_var, n, s) → Case(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s))
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s))
Term_sub(Term_var, Id) → Term_var
Term_sub(Term_var, Cons_usual(m, s)) → m
Term_sub(Term_var, Cons_usual(m, s)) → Term_sub(Term_var, s)
Term_sub(Term_var, Cons_sum(k, s)) → Term_sub(Term_var, s)
Term_sub(Term_sub(m, s), t) → Term_sub(m, Concat(s, t))
Sum_sub(Id) → Sum_term_var
Sum_sub(Cons_sum(k, s)) → Sum_constant(k)
Sum_sub(Cons_sum(k, s)) → Sum_sub(s)
Sum_sub(Cons_usual(m, s)) → Sum_sub(s)
Concat(Concat(s, t), u) → Concat(s, Concat(t, u))
Concat(Cons_usual(m, s), t) → Cons_usual(Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(k, s), t) → Cons_sum(k, Concat(s, t))
Concat(Id, s) → s

Types:
Term_sub :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Case :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Frozen :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Sum_constant:Sum_term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Sum_sub :: Id:Cons_usual:Cons_sum → Sum_constant:Sum_term_var
Sum_constant :: Left:Right → Sum_constant:Sum_term_var
Left :: Left:Right
Right :: Left:Right
Sum_term_var :: Sum_constant:Sum_term_var
Term_app :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_pair :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_inl :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_inr :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_var :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Id :: Id:Cons_usual:Cons_sum
Cons_usual :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
Cons_sum :: Left:Right → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
Concat :: Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
hole_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var1_0 :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
hole_Id:Cons_usual:Cons_sum2_0 :: Id:Cons_usual:Cons_sum
hole_Sum_constant:Sum_term_var3_0 :: Sum_constant:Sum_term_var
hole_Left:Right4_0 :: Left:Right
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0 :: Nat → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
gen_Id:Cons_usual:Cons_sum6_0 :: Nat → Id:Cons_usual:Cons_sum

Lemmas:
Sum_sub(gen_Id:Cons_usual:Cons_sum6_0(n8_0)) → Sum_term_var, rt ∈ Ω(1 + n8₀)
Concat(gen_Id:Cons_usual:Cons_sum6_0(n370_0), gen_Id:Cons_usual:Cons_sum6_0(0)) → gen_Id:Cons_usual:Cons_sum6_0(n370_0), rt ∈ Ω(1 + n370₀)
Term_sub(gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(0), gen_Id:Cons_usual:Cons_sum6_0(n183948_0)) → gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(0), rt ∈ Ω(1 + n183948₀)

Generator Equations:
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(0) ⇔ Term_var
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(+(x, 1)) ⇔ Case(Term_var, gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(x))
gen_Id:Cons_usual:Cons_sum6_0(0) ⇔ Id
gen_Id:Cons_usual:Cons_sum6_0(+(x, 1)) ⇔ Cons_usual(Term_var, gen_Id:Cons_usual:Cons_sum6_0(x))

No more defined symbols left to analyse.

(29) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
Sum_sub(gen_Id:Cons_usual:Cons_sum6_0(n8_0)) → Sum_term_var, rt ∈ Ω(1 + n8₀)

(30) BOUNDS(n^1, INF)

(31) Obligation:

TRS:
Rules:
Term_sub(Case(m, n), s) → Frozen(m, Sum_sub(s), n, s)
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s)
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s)
Frozen(m, Sum_term_var, n, s) → Case(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s))
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s))
Term_sub(Term_var, Id) → Term_var
Term_sub(Term_var, Cons_usual(m, s)) → m
Term_sub(Term_var, Cons_usual(m, s)) → Term_sub(Term_var, s)
Term_sub(Term_var, Cons_sum(k, s)) → Term_sub(Term_var, s)
Term_sub(Term_sub(m, s), t) → Term_sub(m, Concat(s, t))
Sum_sub(Id) → Sum_term_var
Sum_sub(Cons_sum(k, s)) → Sum_constant(k)
Sum_sub(Cons_sum(k, s)) → Sum_sub(s)
Sum_sub(Cons_usual(m, s)) → Sum_sub(s)
Concat(Concat(s, t), u) → Concat(s, Concat(t, u))
Concat(Cons_usual(m, s), t) → Cons_usual(Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(k, s), t) → Cons_sum(k, Concat(s, t))
Concat(Id, s) → s

Types:
Term_sub :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Case :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Frozen :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Sum_constant:Sum_term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Sum_sub :: Id:Cons_usual:Cons_sum → Sum_constant:Sum_term_var
Sum_constant :: Left:Right → Sum_constant:Sum_term_var
Left :: Left:Right
Right :: Left:Right
Sum_term_var :: Sum_constant:Sum_term_var
Term_app :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_pair :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_inl :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_inr :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_var :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Id :: Id:Cons_usual:Cons_sum
Cons_usual :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
Cons_sum :: Left:Right → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
Concat :: Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
hole_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var1_0 :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
hole_Id:Cons_usual:Cons_sum2_0 :: Id:Cons_usual:Cons_sum
hole_Sum_constant:Sum_term_var3_0 :: Sum_constant:Sum_term_var
hole_Left:Right4_0 :: Left:Right
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0 :: Nat → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
gen_Id:Cons_usual:Cons_sum6_0 :: Nat → Id:Cons_usual:Cons_sum

Lemmas:
Sum_sub(gen_Id:Cons_usual:Cons_sum6_0(n8_0)) → Sum_term_var, rt ∈ Ω(1 + n8₀)
Concat(gen_Id:Cons_usual:Cons_sum6_0(n370_0), gen_Id:Cons_usual:Cons_sum6_0(0)) → gen_Id:Cons_usual:Cons_sum6_0(n370_0), rt ∈ Ω(1 + n370₀)

Generator Equations:
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(0) ⇔ Term_var
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(+(x, 1)) ⇔ Case(Term_var, gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(x))
gen_Id:Cons_usual:Cons_sum6_0(0) ⇔ Id
gen_Id:Cons_usual:Cons_sum6_0(+(x, 1)) ⇔ Cons_usual(Term_var, gen_Id:Cons_usual:Cons_sum6_0(x))

No more defined symbols left to analyse.

(32) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
Sum_sub(gen_Id:Cons_usual:Cons_sum6_0(n8_0)) → Sum_term_var, rt ∈ Ω(1 + n8₀)

(33) BOUNDS(n^1, INF)

(34) Obligation:

TRS:
Rules:
Term_sub(Case(m, n), s) → Frozen(m, Sum_sub(s), n, s)
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s)
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s)
Frozen(m, Sum_term_var, n, s) → Case(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s))
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s))
Term_sub(Term_var, Id) → Term_var
Term_sub(Term_var, Cons_usual(m, s)) → m
Term_sub(Term_var, Cons_usual(m, s)) → Term_sub(Term_var, s)
Term_sub(Term_var, Cons_sum(k, s)) → Term_sub(Term_var, s)
Term_sub(Term_sub(m, s), t) → Term_sub(m, Concat(s, t))
Sum_sub(Id) → Sum_term_var
Sum_sub(Cons_sum(k, s)) → Sum_constant(k)
Sum_sub(Cons_sum(k, s)) → Sum_sub(s)
Sum_sub(Cons_usual(m, s)) → Sum_sub(s)
Concat(Concat(s, t), u) → Concat(s, Concat(t, u))
Concat(Cons_usual(m, s), t) → Cons_usual(Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(k, s), t) → Cons_sum(k, Concat(s, t))
Concat(Id, s) → s

Types:
Term_sub :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Case :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Frozen :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Sum_constant:Sum_term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Sum_sub :: Id:Cons_usual:Cons_sum → Sum_constant:Sum_term_var
Sum_constant :: Left:Right → Sum_constant:Sum_term_var
Left :: Left:Right
Right :: Left:Right
Sum_term_var :: Sum_constant:Sum_term_var
Term_app :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_pair :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_inl :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_inr :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Term_var :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Id :: Id:Cons_usual:Cons_sum
Cons_usual :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
Cons_sum :: Left:Right → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
Concat :: Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
hole_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var1_0 :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
hole_Id:Cons_usual:Cons_sum2_0 :: Id:Cons_usual:Cons_sum
hole_Sum_constant:Sum_term_var3_0 :: Sum_constant:Sum_term_var
hole_Left:Right4_0 :: Left:Right
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0 :: Nat → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
gen_Id:Cons_usual:Cons_sum6_0 :: Nat → Id:Cons_usual:Cons_sum

Lemmas:
Sum_sub(gen_Id:Cons_usual:Cons_sum6_0(n8_0)) → Sum_term_var, rt ∈ Ω(1 + n8₀)

Generator Equations:
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(0) ⇔ Term_var
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(+(x, 1)) ⇔ Case(Term_var, gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(x))
gen_Id:Cons_usual:Cons_sum6_0(0) ⇔ Id
gen_Id:Cons_usual:Cons_sum6_0(+(x, 1)) ⇔ Cons_usual(Term_var, gen_Id:Cons_usual:Cons_sum6_0(x))

No more defined symbols left to analyse.

(35) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
Sum_sub(gen_Id:Cons_usual:Cons_sum6_0(n8_0)) → Sum_term_var, rt ∈ Ω(1 + n8₀)

(36) BOUNDS(n^1, INF)